T:Type, L:(T List), x:T. (x  L)  ((null(L))) 

latex

Definitions	t  T, P  Q, x:A. B(x), False, P  Q, Dec(P), A,
Lemmas	l member wf, null member, null wf, decidable assert